Nuprl Definition : es-first-since 11,40

e2 = first e  e1.P(e) == es-le(ese1e2 P(e2 e[e1,e2).P(e
latex



clarification:

es-first-since(es;e.P(e);e1;e2) == es-le(ese1e2 P(e2 alle from es in [e1;e2).P(e
latex


Definitionse2 = first e  e1.P(e), es-le(esee'), P  Q, e[e1,e2).P(e), A
FDL editor aliaseses-first-since

origin